/*******************************************************************\

Module: Concrete Goto Program

Author: Daniel Kroening, kroening@kroening.com

\*******************************************************************/

#ifndef CPROVER_GOTO_PROGRAM_H
#define CPROVER_GOTO_PROGRAM_H

#include <set>

#include <std_code.h>

#include "goto_program_template.h"

//#include "struct/CFA_StructHandle.h"

//#include <cfa/cfa.h>
//#include <cfa/typedef.h>


class goto_programt:public goto_program_templatet<codet, exprt>
{
public:
  std::ostream& output_instruction(
    const class namespacet &ns,
    const irep_idt &identifier,
    std::ostream& out,
    instructionst::const_iterator it) const;

  std::ostream& output_instructionCFA(
    map<string, string> &struct_information,
    const class namespacet &ns,
    const irep_idt &identifier,
    map< instructionst::const_iterator, Node * > &NodeMap,
    map< int, Node * > &LabelMap,
    //vector< Node * > &actual_nodes,
    std::ostream &out,
    instructionst::const_iterator it) const;

  Expr* handle_exprCFA(
  const int flag,
  const class namespacet &ns,
  const irep_idt &identifier,
  const exprt &e) const;

  Prop* handle_propCFA(
  const class namespacet &ns,
  const irep_idt &identifier,
  const exprt &e) const;

  Expr* handle_symCFA(
  const class namespacet &ns,
  const irep_idt &identifier,
  const exprt &e) const;

  void create_unarynode(
  map<string, string> &struct_information,
  const class namespacet &ns,
  const irep_idt &identifier,
  map< instructionst::const_iterator, Node * > &NodeMap,
  map< int, Node * > &LabelMap,
  std::ostream &out,
  instructionst::const_iterator it,
  vector<Node*> &beforenodes,
  StmtType st_type,
  string LabelName ) const;
  
  void create_badnode(
  map< instructionst::const_iterator, Node * > &NodeMap,
  map< int, Node * > &LabelMap,
  std::ostream &out,
  instructionst::const_iterator it,
  vector<Node*> &beforenodes,
  StmtType st_type ) const;

  goto_programt() { }
  
  // get the variables in decl statements
  typedef std::set<irep_idt> decl_identifierst;
  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
};

#define forall_goto_program_instructions(it, program) \
  for(goto_programt::instructionst::const_iterator it=(program).instructions.begin(); \
      it!=(program).instructions.end(); it++)

#define Forall_goto_program_instructions(it, program) \
  for(goto_programt::instructionst::iterator it=(program).instructions.begin(); \
      it!=(program).instructions.end(); it++)
 
bool operator<(const goto_programt::const_targett i1,
               const goto_programt::const_targett i2);

std::list<exprt> objects_read(const goto_programt::instructiont &);
std::list<exprt> objects_written(const goto_programt::instructiont &);

std::list<exprt> expressions_read(const goto_programt::instructiont &);
std::list<exprt> expressions_written(const goto_programt::instructiont &);

#endif
